FDL - Step of Proof: bool-to-neg-dcdr_wf

Step of Proof: bool-to-neg-dcdr_wf

Inference at *
Iof proof for Lemma bool-to-neg-dcdr wf:

A:Type, f:(A

), x:A. {f}

(x)

Dec(f(x) = ff)

by Auto

1:

1: 1. A : Type

1: 2. f : A

1: 3. x : A

1:

{f}

(x)

Dec(f(x) = ff)

.

Definitions x:A. B(x), Dec(P), s = t, f(a), {f}, x:AB(x), , t T, Type

Lemmas bool wf